ArghDA M2: Cubical-Agda backend — the flag-profile island - #36
Merged
Conversation
Cubical Agda (`--cubical --safe`, NOT `--without-K`) as a distinct backend, `agda-cubical`. Implemented as a separate `AgdaCubical` type rather than the plan's `Agda::cubical()` constructor — a distinct type expresses the island better (a `--cubical --safe` file and a `--safe --without-K` file cannot import each other; Agda enforces this at typecheck and arghda surfaces the resulting Error honestly) and avoids churning ~19 `Agda` value-uses. - `src/prover/agda.rs` — `AgdaCubical` shares `invoke_agda()` (which now adds `--cubical`) and all the graph methods with `Agda`; it differs only in name, `safe_mode` (`--cubical --safe`), and lint pack. - `src/lint/safe_pragma.rs` — `SafePragma` is now parameterised by the required OPTIONS flags: `standard()` = `[--safe, --without-K]`, `cubical()` = `[--cubical, --safe]`. A cubical file no longer trips a spurious "missing --without-K" (which would be wrong — cubical is incompatible with it), and a standard file is still flagged if it lacks either. - `src/lint/mod.rs` — `agda_cubical_rules()` swaps in the cubical pragma; the rest of the pack is shared via a private `agda_pack()`. - `src/main.rs` — `--backend agda-cubical` wired; `about`/help updated. ## Verified (ran, not inferred) - `cargo test` → 107 passing, 0 failed (79 lib + 28 integration; +3 safe_pragma unit covering the standard/cubical profile split, +1 cubical-identity unit, +3 cubical integration). - clippy -D warnings, fmt, SPDX clean. - Dogfooded REAL agda: `check --backend agda-cubical` on a `--cubical --safe` file → proven-eligible; the standard `agda` backend on the SAME file → rejected (`missing-safe-pragma: missing --without-K`). The island distinction is demonstrated end-to-end. - STATE.a2ml records M2 = 100%. Five backends now live across both interaction models. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 09:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
Cubical Agda (
--cubical --safe, not--without-K) as a distinct backend,agda-cubical. That completes the Agda family and the fifth backend overall.Design note: implemented as a separate
AgdaCubicaltype rather than the plan'sAgda::cubical()constructor. A distinct type expresses the island better — a--cubical --safefile and a--safe --without-Kfile cannot import each other; Agda enforces this at typecheck and arghda surfaces the resultingErrorhonestly rather than pretending the edge is sound — and it avoids churning ~19Agdavalue-uses across the tree.Changes
src/prover/agda.rs—AgdaCubicalsharesinvoke_agda()(now adds--cubical) and all graph methods withAgda; differs only in name,safe_mode(--cubical --safe), and lint pack.src/lint/safe_pragma.rs—SafePragmais now parameterised by required OPTIONS flags:standard()=[--safe, --without-K],cubical()=[--cubical, --safe]. A cubical file no longer trips a spurious "missing --without-K" (which would be wrong — cubical is incompatible with it), and a standard file is still flagged if it lacks either.src/lint/mod.rs—agda_cubical_rules()swaps in the cubical pragma; the rest of the pack is shared via a privateagda_pack().src/main.rs—--backend agda-cubicalwired;about/help updated.Verified (ran, not inferred)
cargo test→ 107 passing, 0 failed (79 lib + 28 integration; +3 safe_pragma unit covering the standard/cubical split, +1 cubical-identity unit, +3 cubical integration).cargo clippy -D warningsclean ·cargo fmt --checkclean ·check-spdx.shOK.check --backend agda-cubicalon a--cubical --safefile →proven-eligible; the standardagdabackend on the same file →rejected(missing-safe-pragma: missing --without-K). The island distinction demonstrated end-to-end.Milestone status
Five backends live across both interaction models:
agda,agda-cubical,idris2(Assistant);z3,cvc5(Solver). Next: finish M0 (arghda doctor), then M6 (Lean4) / M11 (studio JSON + Groove).Generated by Claude Code